The present application relates generally to an improved data processing apparatus and method and more specifically to mechanisms for formally verifying random priority-based arbiters.
Arbiters are widely used in electronic systems such as micro-processors and interconnects. Arbiters restrict access to shared resources when a number of requests exceeds a maximum number of requests that may be satisfied concurrently. For example, an arbiter that regulates access to a bus selects which requestors would be granted access to the bus if there are more concurrent requests than the bus can handle. Arbiters use various arbitration schemes in the form of a priority function to serialize access to the shared resource by the requestors. The priority function decides which requestor to grant access next. Examples of priority functions include round robin (rotate priority amongst requestors), queue-based (first-in first-out), or random priority-based (select next requestor randomly).
Random priority-based arbiters have been gaining in popularity because of their high potential for fair arbitration, unlike other techniques such as round robin or queue-based which may be unfair because of their fixed order of arbitration. Random priority-based arbitration allows any request to have the highest priority at random. A random priority-based arbiter uses a pseudo-random number generator to select or influence the selection of the next requestor. A common implementation of such arbiters uses a Linear Feedback Shift Register (LFSR) to generate a pseudo-random sequence of numbers. A LFSR is a cyclic shift register whose current state is a linear function of its previous state, and the LFSR generates a sequence of numbers which is statistically similar to a truly-random sequence.